\begin{tabbing}
$\vdash$  \=$\forall$$A$:Type, $f$:($A$$\rightarrow$($A$ + Top)), $x$:$A$, $m$, $n$:$\mathbb{N}$.\+
\\[0ex]($\uparrow$can{-}apply($f$\^{}$m$;$x$)) $\Rightarrow$ (($f$\^{}$n$+$m$($x$)) $\sim$ ($f$\^{}$n$(do{-}apply($f$\^{}$m$;$x$))))
\-
\end{tabbing}